the_w:World.
FairFifo
 (m:, l:IdLnk, t:. (m  ||snds(l;t)||)  (t':. ((t  t') & (m  ||rcvs(l;t')||)))) 

latex

Definitions

, t  T, x:AB(x), IdLnk, A  B, x:A  B(x), P & Q, x:A. B(x), P  Q, x:A. B(x), FairFifo, World, {x:A| B(x)} , i  j , a < b, Void, False, A, #$n, -n, n+m, n - m, rcvs(l;t), destination(l), Action(i), ||as||, , snds(l;t), Msg, , A c B, left + right, P  Q, b, s = t, b, , (i = j), P  Q, Unit, {T}, SQType(T), s ~ t, a(i;t), isrcv(l;a), x:A.B(x), Top, upto(n), {i..j}, i  j < k, x.A(x), Type, map(f;as), True, type List, [], [car / cdr], P  Q, T, S  T, queue(l;t), i z j, i <z j, if b then t else f fi , m(l;t)

Lemmas

concat iseg, w-ml wf, assert of lt int, bnot of lt int, assert of le int, lt int wf, le int wf, general length nth tl, top wf, length zero, filter iseg, iseg map, upto iseg, iseg length, squash wf, true wf, length append, map append sq, filter append sq, map wf, int seg wf, upto wf, w-isrcvl wf, w-a wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, not wf, assert wf, IdLnk wf, non neg length, w-Msg wf, w-snds wf, le wf, length wf1, w-action wf, ldst wf, w-rcvs wf, ge wf, nat properties, world wf, fair-fifo wf, nat wf